package hu.ngms.jpf.examples;

import gov.nasa.jpf.annotation.Ensures;
import gov.nasa.jpf.annotation.Invariant;
import gov.nasa.jpf.annotation.Requires;

@Invariant("messagesLogged >= 0")
public class DesignByContract {

	private int messagesLogged;

	@Requires("message != null")
	@Ensures("old(messagesLogged) < messagesLogged")
	public void log(String message, boolean ensuresOk) {
		System.out.println("[" + messagesLogged + "] " + System.currentTimeMillis() + " " + message);
		if (ensuresOk) {
			messagesLogged++;
		} else {
			messagesLogged--;
		}
	}

}
